es:ES, Sys:AbsInterface(Top), f:(E(Sys)E(Sys)). sys-order(es; Sys; f)   

latex

Up	abstract chain replication
Definitions of Statement	sys-order(es; Sys; f)
Definitions	sys-order(es; Sys; f), e  X, Atom$n, False, (e < e'), y=f*(x) via L, hd(l), x:A. B(x), loc(e), t.1, let x,y = A in B(x;y), {x:A| B(x)} , (e <loc e'), y is f*(x), AbsInterface(A), E(X), E, P & Q, x. t(x), x.A(x), pred(e), <a, b>, A, first(e), suptype(S; T), S  T, Top, x:A.B(x), !Void(), x,y. t(x;y), pred!(e;e'), , SWellFounded(R(x;y)), constant_function(f;A;B), b, , e < e', r  s, val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), , type List, Msg(M), kind(e), loc(e), Knd, kindcase(k; a.f(a); l,t.g(l;t) ), EOrderAxioms(E; pred?; info), x:A  B(x), IdLnk, left + right, Unit, EqDecider(T), Type, P  Q, strong-subtype(A;B), , Id, f(a), a:A fp B(a), EState(T), ES, x:A. B(x), x:AB(x), t  T, s = t
Lemmas	event system wf, subtype rel wf, EState wf, Id wf, rationals wf, member wf, strongwellfounded wf, pred! wf, unit wf, top wf, first wf, assert wf, not wf, loc wf, constant function wf, IdLnk wf, kindcase wf, Knd wf, bool wf, qle wf, cless wf, val-axiom wf, nat wf, Msg wf, kind wf, EOrderAxioms wf, deq wf, es-E wf, es-E-interface wf, es-locl wf, es-causl wf, es-loc wf, false wf, fun-connected wf, fun-path wf, es-is-interface wf, es-interface wf